Nuprl Definition : atom-free-decl 11,40

AtomFree(d) == xdom(d). A=d(x)   AtomFree(Type;A) 
latex



clarification:

atom-free-decl{i:l}(T; eq; d) == Teqxdom(d). A=d(x)   atom-free{1:n}(Type{i}; A) 
latex


DefinitionsType, xdom(f). v=f(x)   P(x;v)
FDL editor aliasesatom-free-decl

origin